es:ES, T:(i:Idk:Kndkindtype(i;k)es_state(es;i)es_state(es;i)),
S:(i:Idk:Kndkindtype(i;k)state@i(Msg List)),
C:(i,b:Idstate@i(?kindtype(i;locl(b)))).
((e:E. (timed)state after e = T(loc(e),kind(e),val(e),es_state_when(es;e)))
& (e:E.
& ((islocal(kind(e)))
& ( (n:
& ( (((isl(C(loc(e),act(kind(e)),n,(state when e))))
& ( (c (val(e) = outl(C(loc(e),act(kind(e)),n,(state when e)))  valtype(e)))))
& (e:E.
& ((isrcv(kind(e)))
& ( (<lnk(kind(e)), tag(kind(e)), val(e)>  S
& ( (<lnk(kind(e)), tag(kind(e)), val(e)>  (loc(sender(e))
& ( (<lnk(kind(e)), tag(kind(e)), val(e)>  ,kind(sender(e))
& ( (<lnk(kind(e)), tag(kind(e)), val(e)>  ,val(sender(e))
& ( (<lnk(kind(e)), tag(kind(e)), val(e)>  ,(state when sender(e))))))
 (a:Atom1, e:E.
 (T(loc(e)):k:Kndkindtype(loc(e);k)es_state(es;loc(e))es_state(es;loc(e))||a
 ( C(loc(e)):b:Idstate@loc(e)(?kindtype(loc(e);locl(b)))||a
 ( ((first(e)))
 ( es_state_when(es;pred(e)):es_state(es;loc(pred(e)))||a
 ( ((isrcv(pred(e)))  val(pred(e)):valtype(pred(e))||a)
 ( es_state_when(es;e):es_state(es;loc(e))||a)
 & (S(loc(e)):k:Kndkindtype(loc(e);k)state@loc(e)(Msg List)||a
 & ( C(loc(e)):b:Idstate@loc(e)(?kindtype(loc(e);locl(b)))||a
 & ( (state when e):state@loc(e)||a
 & ( ((isrcv(e))  val(e):valtype(e)||a)
 & ( e sends || a)) 

latex

Definitions

ES, Knd, type List, state@i, e sends || a, x:T||a, es_state(es;i), (timed)state after e, es_state_when(es;e), P & Q, islocal(k), x:A. B(x), A c B, isl(x), s = t, outl(x), Unit, left + right, E, , Type, isrcv(k), (x  l), f(a), loc(e), kind(e), (state when e), sender(e), , {x:A| B(x)} , , A  B, A, False, locl(a), act(k), P  Q, S  T, lnk(k), <a, b>, tag(k), Msg, x:A  B(x), Id, IdLnk, x:A. B(x), x:AB(x), val(e), t  T, kindtype(i;k), valtype(e), b, Atom$n, first(e), pred(e), isrcv(e), r - s, time(e), SQType(T), {T}, s ~ t, s+r, x. t(x), x.A(x), es_vartype(es;i;x), T, P  Q, P  Q, e loc e' , let x,y = A in B(x;y), True, x,y:A//B(x;y), x,y. t(x;y), qeq(r;s), , EquivRel(T;x,y.E(x;y)), , A  B, , t.1, a < b, if b then t else f fi , Dec(P), P  Q, Top, x:A.B(x), Void, x when e, s(now), es-M(es), t.2, emsg(e), rcvtype(e), b, msg(l;t;v), Msg(M), constant_function(f;A;B), r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), kindcase(k; a.f(a); l,t.g(l;t) ), EState(T), EOrderAxioms(E; pred?; info), EqDecider(T), acttype(e)

Lemmas

es-rcvtype wf, subtype rel self, tagof wf, lnk wf, es-M wf, squash wf, es-msg wf, free-from-atom-l member, bnot wf, bool wf, eqff to assert, iff transitivity, eqtt to assert, es-read-state wf, free-from-atom-Id, free-from-atom-nat, true wf, false wf, top wf, free-from-atom-outl, assert of bnot, islocal-not-isrcv, decidable assert, Id sq, es-valtype-kindtype, free-from-atom-Knd, qeq wf2, quotient wf, es-loc-pred, es-le-loc, es-isrcv-loc, es vartype wf, subtype rel dep function, es-shift wf2, qsub wf, int-rational, free-from-atom-rational, state-after-pred, es-isrcv wf, free-from-atom wf1, es-pred wf, es-first wf, not wf, es-val wf, actof wf, locl wf, es-kindtype wf, es-sender wf, es-state-when wf, es-kind wf, es-loc wf, es-Msg wf, l member wf, isrcv wf, assert wf, unit wf, outl wf, es-valtype wf, isl wf, nat wf, islocal wf, es state when wf, es state after wf, es state wf, es-E wf, es-state wf, Knd wf, Id wf, event system wf